Theory Case_Labeling

theory Case_Labeling
imports Main
keywords "print_nested_cases" :: diag
begin

section ‹Labeling Subgoals›

context begin
  qualified type_synonym prg_ctxt_var = unit
  qualified type_synonym prg_ctxt = "string × nat × prg_ctxt_var list"

  text ‹Embed variables in terms›
  qualified definition VAR :: "'v  prg_ctxt_var" where
    "VAR _ = ()"

  text ‹Labeling of a subgoal›
  qualified definition VC :: "prg_ctxt list  'a  'a" where
    "VC ct P  P"

  text ‹Computing the statement numbers and context›
  qualified definition CTXT :: "nat  prg_ctxt list  nat  'a  'a" where
    "CTXT inp ct outp P  P"

  text ‹Labeling of a term binding or assumption›
  qualified definition BIND :: "string  nat  'a  'a" where
    "BIND name inp P  P"

  text ‹Hierarchy labeling›
  qualified definition HIER :: "prg_ctxt list  'a  'a" where
    "HIER ct P  P"

  text ‹Split Labeling. This is used as an assumption›
  qualified definition SPLIT :: "'a  'a  bool" where
    "SPLIT v w  v = w"

  text ‹Disambiguation Labeling. This is used as an assumption›
  qualified definition DISAMBIG :: "nat  bool" where
    "DISAMBIG n  True"

  lemmas LABEL_simps = BIND_def CTXT_def HIER_def SPLIT_def VC_def

  lemma Initial_Label: "CTXT 0 [] outp P  P"
    by (simp add: Case_Labeling.CTXT_def)

  lemma
    BIND_I: "P  BIND name inp P" and
    BIND_D: "BIND name inp P  P" and
    VC_I: "P  VC ct P"
    unfolding Case_Labeling.BIND_def Case_Labeling.VC_def .

  lemma DISAMBIG_I: "(DISAMBIG n  P)  P"
    by (auto simp: DISAMBIG_def Case_Labeling.VC_def)

  lemma DISAMBIG_E: "(DISAMBIG n  P)  P"
    by (auto simp: DISAMBIG_def)

  text ‹Lemmas for the tuple postprocessing›
  lemma SPLIT_reflection: "SPLIT x y  (x  y)"
    unfolding SPLIT_def by (rule eq_reflection)

  lemma rev_SPLIT_reflection: "(x  y)  SPLIT x y"
    unfolding SPLIT_def ..

  lemma SPLIT_sym: "SPLIT x y  SPLIT y x"
    unfolding SPLIT_def by (rule sym)

  lemma SPLIT_thin_refl: "SPLIT x x; PROP W  PROP W" .

  lemma SPLIT_subst: "SPLIT x y; P x  P y"
    unfolding SPLIT_def by hypsubst

  lemma SPLIT_prodE:
    assumes "SPLIT (x1, y1) (x2, y2)"
    obtains "SPLIT x1 x2" "SPLIT y1 y2"
    using assms unfolding SPLIT_def by auto


end

text ‹
  The labeling constants were qualified to not interfere with any other theory.
  The following locale allows using a nice syntax in other theories
›

locale Labeling_Syntax begin
  abbreviation VAR where "VAR  Case_Labeling.VAR"
  abbreviation VC ("V⟨(2_,_:/ _)") where "VC bl ct   Case_Labeling.VC (bl # ct)"
  abbreviation CTXT ("C⟨(2_,_,_:/ _)") where "CTXT  Case_Labeling.CTXT"
  abbreviation BIND ("B⟨(2_,_:/ _)") where "BIND  Case_Labeling.BIND"
  abbreviation HIER ("H⟨(2_:/ _)") where "HIER  Case_Labeling.HIER"
  abbreviation SPLIT where "SPLIT  Case_Labeling.SPLIT"
end

text ‹Lemmas for converting terms from @{term Suc}/@{term "0::nat"} notation to numerals›
lemma Suc_numerals_conv:
  "Suc 0 = Numeral1"
  "Suc (numeral n) = numeral (n + num.One)"
  by auto

lemmas Suc_numeral_simps = Suc_numerals_conv add_num_simps


section ‹Casify›

text ‹
  Introduces a command @{command print_nested_cases}. This is similar to @{command print_cases},
  but shows also the nested cases.
›
ML_file ‹print_nested_cases.ML›

ML_file ‹util.ML›

text ‹Introduces the proof method.›
ML_file ‹casify.ML›


ML val casify_defs = Casify.Options { simp_all_cases=true, split_right_only=true, protect_subgoals=false }

method_setup prepare_labels = Scan.succeed (fn ctxt => SIMPLE_METHOD (ALLGOALS (Casify.prepare_labels_tac ctxt))) "VCG labelling: prepare labels"

method_setup casify = Casify.casify_method_setup casify_defs
  "VCG labelling: Turn the labels into cases"

end