equal
deleted
inserted
replaced
952 |
952 |
953 lemmas list_ext_simps = list_ext_lt_get list_ext_lt list_ext_len list_ext_len_eq |
953 lemmas list_ext_simps = list_ext_lt_get list_ext_lt list_ext_len list_ext_len_eq |
954 |
954 |
955 lemma listsum_upd_suc: |
955 lemma listsum_upd_suc: |
956 "a < length ks \<Longrightarrow> listsum (map Suc (ks[a := Suc (ks ! a)]))= (Suc (listsum (map Suc ks)))" |
956 "a < length ks \<Longrightarrow> listsum (map Suc (ks[a := Suc (ks ! a)]))= (Suc (listsum (map Suc ks)))" |
957 by (smt Ex_list_of_length Skolem_list_nth elem_le_listsum_nat |
957 by (smt elem_le_listsum_nat |
958 length_induct length_list_update length_map length_splice |
958 length_list_update list_ext_get_upd |
959 list_eq_iff_nth_eq list_ext_get_upd list_ext_lt_get list_update_beyond |
959 list_update_overwrite listsum_update_nat map_update |
960 list_update_id list_update_overwrite list_update_same_conv list_update_swap |
960 nth_equalityI nth_list_update nth_map) |
961 listsum_update_nat map_eq_imp_length_eq map_update neq_if_length_neq |
|
962 nth_equalityI nth_list_update nth_list_update_eq nth_list_update_neq nth_map reps_sep_len_def) |
|
963 |
961 |
964 lemma reps_len_suc: |
962 lemma reps_len_suc: |
965 assumes "a < length ks" |
963 assumes "a < length ks" |
966 shows "reps_len (ks[a:=Suc(ks!a)]) = 1 + reps_len ks" |
964 shows "reps_len (ks[a:=Suc(ks!a)]) = 1 + reps_len ks" |
967 proof(cases "length ks \<le> 1") |
965 proof(cases "length ks \<le> 1") |
1913 fun mk_ps_term x = |
1911 fun mk_ps_term x = |
1914 Const (@{const_name ps}, @{typ "int \<Rightarrow> tresource set \<Rightarrow> bool"}) $ Free (x, @{typ "int"}) |
1912 Const (@{const_name ps}, @{typ "int \<Rightarrow> tresource set \<Rightarrow> bool"}) $ Free (x, @{typ "int"}) |
1915 |
1913 |
1916 fun atomic tac = ((SOLVED' tac) ORELSE' (K all_tac)) |
1914 fun atomic tac = ((SOLVED' tac) ORELSE' (K all_tac)) |
1917 |
1915 |
|
1916 fun map_simpset f = Context.proof_map (Simplifier.map_ss f) |
|
1917 |
1918 fun pure_sep_conj_ac_tac ctxt = |
1918 fun pure_sep_conj_ac_tac ctxt = |
1919 (auto_tac (ctxt |> Simplifier.map_simpset (fn ss => ss addsimps @{thms sep_conj_ac})) |
1919 (auto_tac (map_simpset (fn ss => ss addsimps @{thms sep_conj_ac}) ctxt) |
1920 |> SELECT_GOAL) |
1920 |> SELECT_GOAL) |
1921 |
1921 |
1922 |
1922 |
1923 fun potential_facts ctxt prop = Facts.could_unify (Proof_Context.facts_of ctxt) |
1923 fun potential_facts ctxt prop = Facts.could_unify (Proof_Context.facts_of ctxt) |
1924 ((Term.strip_all_body prop) |> Logic.strip_imp_concl); |
1924 ((Term.strip_all_body prop) |> Logic.strip_imp_concl); |
1926 fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => |
1926 fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => |
1927 (Method.insert_tac (potential_facts ctxt goal) i) THEN |
1927 (Method.insert_tac (potential_facts ctxt goal) i) THEN |
1928 (pure_sep_conj_ac_tac ctxt i)); |
1928 (pure_sep_conj_ac_tac ctxt i)); |
1929 |
1929 |
1930 fun sep_conj_ac_tac ctxt = |
1930 fun sep_conj_ac_tac ctxt = |
1931 (SOLVED' (auto_tac (ctxt |> Simplifier.map_simpset (fn ss => ss addsimps @{thms sep_conj_ac})) |
1931 (SOLVED' (auto_tac (ctxt |> map_simpset (fn ss => ss addsimps @{thms sep_conj_ac})) |
1932 |> SELECT_GOAL)) ORELSE' (atomic (some_fact_tac ctxt)) |
1932 |> SELECT_GOAL)) ORELSE' (atomic (some_fact_tac ctxt)) |
1933 *} |
1933 *} |
1934 |
1934 |
1935 ML {* |
1935 ML {* |
1936 type HoareTriple = { |
1936 type HoareTriple = { |
2337 val reordered = FunApp.fun_app_free reordered_skel state |> HOLogic.mk_Trueprop |
2337 val reordered = FunApp.fun_app_free reordered_skel state |> HOLogic.mk_Trueprop |
2338 val goal = Logic.mk_implies |
2338 val goal = Logic.mk_implies |
2339 (if conclusion then (orig, reordered) else (reordered, orig)); |
2339 (if conclusion then (orig, reordered) else (reordered, orig)); |
2340 val rule = |
2340 val rule = |
2341 Goal.prove ctxt [] [] goal (fn _ => |
2341 Goal.prove ctxt [] [] goal (fn _ => |
2342 auto_tac (ctxt |> Simplifier.map_simpset (fn ss => ss addsimps @{thms sep_conj_ac}))) |
2342 auto_tac (ctxt |> map_simpset (fn ss => ss addsimps @{thms sep_conj_ac}))) |
2343 |> Drule.export_without_context |
2343 |> Drule.export_without_context |
2344 in |
2344 in |
2345 rule |
2345 rule |
2346 end |
2346 end |
2347 *} |
2347 *} |